Nuprl Definition : same_order 4,23

same_order(x1;y1;x2;y2;L;T) == x1 << y1  L  (x2  L)  (y2  L)  x2 << y2  L 
latex



clarification:

same_order(x1;y1;x2;y2;L;T)
== strong_before(x1; y1; L; T)  (x2  L  T)  (y2  L  T)  strong_before(x2; y2; L; T) 
latex


DefinitionsP  Q, (x  l), x << y  l
FDL editor aliasessame_order

origin